|
| 1: |
|
and(true,y) |
→ y |
| 2: |
|
and(false,y) |
→ false |
| 3: |
|
eq(nil,nil) |
→ true |
| 4: |
|
eq(cons(t,l),nil) |
→ false |
| 5: |
|
eq(nil,cons(t,l)) |
→ false |
| 6: |
|
eq(cons(t,l),cons(t',l')) |
→ and(eq(t,t'),eq(l,l')) |
| 7: |
|
eq(var(l),var(l')) |
→ eq(l,l') |
| 8: |
|
eq(var(l),apply(t,s)) |
→ false |
| 9: |
|
eq(var(l),lambda(x,t)) |
→ false |
| 10: |
|
eq(apply(t,s),var(l)) |
→ false |
| 11: |
|
eq(apply(t,s),apply(t',s')) |
→ and(eq(t,t'),eq(s,s')) |
| 12: |
|
eq(apply(t,s),lambda(x,t)) |
→ false |
| 13: |
|
eq(lambda(x,t),var(l)) |
→ false |
| 14: |
|
eq(lambda(x,t),apply(t,s)) |
→ false |
| 15: |
|
eq(lambda(x,t),lambda(x',t')) |
→ and(eq(x,x'),eq(t,t')) |
| 16: |
|
if(true,var(k),var(l')) |
→ var(k) |
| 17: |
|
if(false,var(k),var(l')) |
→ var(l') |
| 18: |
|
ren(var(l),var(k),var(l')) |
→ if(eq(l,l'),var(k),var(l')) |
| 19: |
|
ren(x,y,apply(t,s)) |
→ apply(ren(x,y,t),ren(x,y,s)) |
| 20: |
|
ren(x,y,lambda(z,t)) |
→ lambda(var(cons(x,cons(y,cons(lambda(z,t),nil)))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t))) |
|
There are 16 dependency pairs:
|
| 21: |
|
EQ(cons(t,l),cons(t',l')) |
→ AND(eq(t,t'),eq(l,l')) |
| 22: |
|
EQ(cons(t,l),cons(t',l')) |
→ EQ(t,t') |
| 23: |
|
EQ(cons(t,l),cons(t',l')) |
→ EQ(l,l') |
| 24: |
|
EQ(var(l),var(l')) |
→ EQ(l,l') |
| 25: |
|
EQ(apply(t,s),apply(t',s')) |
→ AND(eq(t,t'),eq(s,s')) |
| 26: |
|
EQ(apply(t,s),apply(t',s')) |
→ EQ(t,t') |
| 27: |
|
EQ(apply(t,s),apply(t',s')) |
→ EQ(s,s') |
| 28: |
|
EQ(lambda(x,t),lambda(x',t')) |
→ AND(eq(x,x'),eq(t,t')) |
| 29: |
|
EQ(lambda(x,t),lambda(x',t')) |
→ EQ(x,x') |
| 30: |
|
EQ(lambda(x,t),lambda(x',t')) |
→ EQ(t,t') |
| 31: |
|
REN(var(l),var(k),var(l')) |
→ IF(eq(l,l'),var(k),var(l')) |
| 32: |
|
REN(var(l),var(k),var(l')) |
→ EQ(l,l') |
| 33: |
|
REN(x,y,apply(t,s)) |
→ REN(x,y,t) |
| 34: |
|
REN(x,y,apply(t,s)) |
→ REN(x,y,s) |
| 35: |
|
REN(x,y,lambda(z,t)) |
→ REN(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)) |
| 36: |
|
REN(x,y,lambda(z,t)) |
→ REN(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t) |
|
The approximated dependency graph contains 2 SCCs:
{22-24,26,27,29,30}
and {33-36}.